<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
  <meta content="text/html; charset=ISO-8859-1"
 http-equiv="content-type">
  <title>README</title>
</head>
<body style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);"
 vlink="#ff0000" alink="#000088" link="#0000ff">
<small><code>//********************************************************************/<br>
//* Copyright (C) 2005 thru 2011 &nbsp; &nbsp; &nbsp; &nbsp;
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
*/<br>
//* MEL O'CAT : x178g243 at yahoo.com &nbsp;&nbsp;&nbsp;&nbsp; &nbsp;
&nbsp; &nbsp; &nbsp; &nbsp;&nbsp;
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
*/<br>
//* License terms: GNU General Public License Version
2&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
*/<br>
//*&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
or
any
later
version&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
*/<br>
//********************************************************************/<br>
//*4567890123456 (71-character line to adjust editor window) 23456789*/<br>
</code></small><br>
<h3>As Of 1-Nov-2011</h3>
<br>
<big style="font-weight: bold;">For Info about the latest release
features click on:<br>
</big>
<ul>
  <li><big style="font-weight: bold;"><a href="CHGLOG.TXT">CHGLOG.TXT</a></big></li>
  <li><big style="font-weight: bold;"><a
 href="doc/mmj2CommandLineArguments.html">mmj2CommandLineArguments.html
    </a></big></li>
  <li><big style="font-weight: bold;"><a href="doc%5CGMFFDoc">mmj2\doc\GMFFDoc\*</a></big></li>
  <li><big style="font-weight: bold;"><a href="mmj2.html">mmj2.html</a>
    </big></li>
</ul>
See also: <big><a style="font-weight: bold;" href="QuickStart.html">QuickStart.html</a></big>&nbsp;
And
<big style="font-weight: bold;"><a href="README.html">README.html</a></big><br>
<br>
<hr style="width: 100%; height: 2px;"><br>
<big><span
 style="font-weight: bold; font-style: italic; color: rgb(0, 153, 0);">You
can
now
support
mmj2
development
with
$$$ donations via Paypal to siskiyousis at gmail.com!<br>
<br>
<span style="color: rgb(204, 0, 0);">And, for questions, bugs,
enhancements, etc. contact Mel at X178G243 at yahoo.com</span></span><br
 style="font-weight: bold; font-style: italic; color: rgb(0, 153, 0);">
</big><big style="font-weight: bold;"><br>
</big><big style="font-weight: bold;"><span
 style="font-family: monospace; color: rgb(0, 102, 0);"></span></big>
<hr style="width: 100%; height: 2px;"><big style="font-weight: bold;"><span
 style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;
-----------------------------------------------------------------</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;
Quick
Start CHEAT SHEET!!!&nbsp; (see also mmj2\QuickStart.html)</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;
-----------------------------------------------------------------&nbsp;&nbsp;&nbsp;
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Quick
Start!!!:</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Windows:&nbsp;
Double-click <code>mmj2\mmj2jar\mmj2.bat</code> in
Windows Explorer</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Mac
OS-X: Double-click mmj2\mmj2jar\MacMMJ2.command in Finder</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
BUT...WAIT!...before
running mmj2, edit, if needed:</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
EDIT--&gt;Windows&nbsp;&nbsp;&nbsp;
mmj2\mmj2jar\RunParms.txt</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
using&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
mmj2\mmj2jar\mmj2.bat</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Notepad:&nbsp;&nbsp;
mmj2\mmj2jar\mmj2PATutorial.bat</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
--&gt;Mac
OS-X&nbsp;&nbsp; mmj2\mmj2jar\RunParms.txt</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
using&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
mmj2\mmj2jar\MacRunParmsPATutorial.txt&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
TextEdit:&nbsp;
mmj2\mmj2jar\MacMMJ2.command</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
mmj2\mmj2jar\MacMMJ2PATutorial.command</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
(Double-click
works well now because the new "mmj2 Fail Popup</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
Window"
*not only* provides start-up and "fail" error</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
messages,
but it also forces the Windows Command Prompt (Mac</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
OS-X
utilities\terminal.app) window to stay open, which makes</span><br
 style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
it
possible to see all of the mmj2 output about the error.)</span></big><big
 style="font-weight: bold;"><br>
</big>
<hr style="width: 100%; height: 2px;"><big style="font-weight: bold;"><br>
0.</big> <span style="font-weight: bold;">mmj2</span>
The key idea of mmj2 and its Proof Assistant -- why you want it
--&nbsp; is that it has a "GUI" Proof Assistant which is said to be
much easier to use than Metamath.exe.<br>
<br>
mmj2 provides a set of tools designed for use <span
 style="font-style: italic;">with</span> <code>Metamath.exe</code> and
its
associated utilities, such as <code>eimm.exe</code>
(Import/Export mmj2 Proof
Worksheet). In addition to the new and improved mmj2 Proof Assistant
GUI -- by far, the
most interesting and useful part of mmj2 -- the mmj2 software package
provides capabilities such as validation of .mm files; proof
verification; grammatical/syntax analysis of .mm files; printing; Text
Mode Formula Formatting&nbsp; ("TMFF"), a novel "pretty printing"
feature that may facilitate comprehension of
complicated math and logic formulas
written in Metamath's ASCII shorthand; and<span
 style="font-weight: bold;"> MUCH MORE...<br>
<br>
</span><big style="font-weight: bold;">1.</big> <span
 style="font-weight: bold;">Installation:</span> Refer
to <a href="INSTALL.html">INSTALL.html</a> for
instructions on installing and taking the next steps to run and use
mmj2. Then visit or return to <a href="mmj2.html">mmj2.html</a> to see
the other documentation,
such as the <a href="doc/PAUserGuide/Start.html">mmj2 Proof Assistant
User Guide</a>. Once you have installed mmj2 be sure to try the
interactive <a href="mmj2jar/mmj2PATutorial.bat">mmj2
Proof
Assistant
Tutorial</a> (which ought to take about an hour.)<br>
<br>
<br>
<big><span style="font-weight: bold;">2.</span></big> <span
 style="font-weight: bold;">Requirements:</span> <br>
<ul>
  <li>You should have a modern PC or Mac/Unix/Linux computer with at
least <span style="text-decoration: underline;">2GB of memory</span>
and a good,
fast
hard drive for a good experience using mmj2, which is a bit of a
memory hog and is processor-intensive after start-up. mmj2, like
Metamath.exe, loads an entire Metamath .mm database (file) into memory
(and then does an unbelievable amount of computation!)</li>
  <li>You will also need <span style="text-decoration: line-through;">Sun
Microsystem's</span> Oracle's <span style="text-decoration: underline;">Java</span>,
either
the
Java
Development
Kit
(<span style="text-decoration: underline;">JDK</span>
aka "J2SE") <span style="text-decoration: underline;">or</span> the
Java Runtime Environment (<span style="text-decoration: underline;">JRE</span>),
version







    <span style="text-decoration: underline;">1.5 or higher</span>.</li>
  <li><span style="text-decoration: underline;">Metamath</span>
itself, is technically speaking, optional, but in practice a necessity
because mmj2 is an add-on, complementary toolkit for Metamath.</li>
  <li>An excellent <a href="http://www.textpad.com/"><span
 style="text-decoration: underline;">text
editor</span></a> capable of handling large files and Unix-style
line endings (even in Windows) is a necessity. See <a
 href="INSTALL.html">INSTALL.html</a> for additional info about
this.</li>
  <li>A file compression utility such as <a
 href="http://www.7-zip.org/">7-Zip</a>.<br>
  </li>
</ul>
<br>
<big style="font-weight: bold;">3.</big> <span
 style="font-weight: bold;">Limitations:</span>&nbsp; mmj2 is still in
"developmental" status, meaning that it is subject to change, bug fixes
and continuing enhancements...at the whim of Mel L. O'Cat (If you don't
like the changes you can clone mmj2 under the GNU GENERAL PUBLIC
LICENSE and write your own code.) <span
 style="font-weight: bold; font-style: italic; text-decoration: underline; color: rgb(153, 0, 0);">There
is
NO
WARRANTY</span>
-- see <a href="LICENSE.TXT">LICENSE.TXT</a> (GNU GENERAL PUBLIC
LICENSE Version 2, June 1991). Use at your own risk. (In any case, you
are <span style="text-decoration: underline;">strongly</span> urged to
always backup your data; to secure your machine from hackers and
viruses, <span style="text-decoration: underline;">whether or not</span>
you use mmj2; to feed your PC only clean electricity from a
battery-powered UPS; <span style="font-style: italic;">and</span> ...
to <span style="font-style: italic;">always</span>
remember that the only secure computer is one that is unplugged,
re-packed in its original shipping container, and safely stacked in a
secure warehouse. I recommend using a firewall such as <a
 href="http://us.norton.com/internet-security/">Norton</a> which allows
you to specify which programs are allowed to access the internet -- and
then to block Java from internet access...better yet, disconnect your
computer from the internet while you are using mmj2 :-) Better safe
than sorry!)<br>
<br>
<br>
<big style="font-weight: bold;">4.</big> <span
 style="font-weight: bold;">Opportunities:</span>
mmj2 was begun as an experimental study of Metamath, and development
has proceed in stages, with each new enhancement package designed to be
as modular and independent from the others as possible. These
developmental stages -- from .mm database validation and printing,
proof verification, grammatical analysis, "proof assistanting", Text
Mode Formula Formatting, etc. -- have advanced the state of&nbsp;
the art of Metamath programming by a small amount and provide a
foundation
for further
work. mmj2 is now usable (and almost good enough to throw away and
rewrite
properly!) But there is still more
work,
more experimentation and more learning to be
done.&nbsp; <br>
<br>
mmj2's capabilities are invoked using "RunParm" commands that form a
language, albeit without looping or "if" statements. Thus, it is easy
to enhance and
extend mmj2, even for "one offs": code a new program, a
new "RunParm" command or two, and modify the mmj.util.BatchMMJ2.java
program, and one can immediately gain programmatic access to a
fully parsed, proof-verified Metamath database loaded into memory and
ready for use. (Note: the <a href="doc%5Cmmj2service">MMJ2 Service</a>
Feature allows your program to call mmj2 or to be called by mmj2.)<br>
<br>
<br>
<big><span style="font-weight: bold;">5.</span></big> <span
 style="font-weight: bold;">Shortcomings of mmj2:</span><br>
<ul>
  <li>It is not a "prover".</li>
  <li>It does not update Metamath .mm databases.</li>
  <li>Its grammatical analysis module does minimal checking for
grammatical ambiguity (this section is stubbed out -- very difficult,
requiring lots of work in special cases because the general case is
impossible to prove :).</li>
  <li>It is a single-user system, not designed for concurrent access
throughout (but you can run more than one instance of mmj2's Proof
Assistant GUI simultaneously.)<br>
  </li>
  <li>All messages are output in English.<br>
  </li>
  <li>All output is left-to-right.</li>
  <li>Support for Unicode or non-ASCII input/output is minimal.</li>
  <li>Metamath RPN-format proofs are only output in the Metamath
uncompressed format.</li>
  <li>Severe data validation errors encountered during start-up, such
as a Metamath .mm database parse error produce error messages on the
operating system Command Prompt window, as well as the mmj2 Fail Popup
Window -- and when you click "ok", processing terminates immediately.
Unfortunately, some users will find these messages hard to decipher.<br>
  </li>
  <li>A redesign could make better use of the various Metamath software
"objects". To a great extent the "objects" are treated mostly as
information hiders and as a way to package program functions written
"old school" style.</li>
  <li>The mmj2 object hierarchy -- <code>Stmt &lt;- Hyp &lt; VarHyp</code>,
etc.
--&nbsp;
has
proven
to
be
resilient
and
extensible.
However, it is clear the Axiom should be subclassed with SyntaxAxiom
(and perhaps Definition!),
which could easily be accomplished if we knew the grammatical Type
Codes at file load time. Also, Proof should be an object in its own
right. (Other design decisions are dubious and/or debatable.)<br>
  </li>
  <li><code>mmj.verify.GRForest.java</code> and <code>GRNode.java</code>
can be replaced with a Java <code>TreeSet</code> (they are no longer
needed except for duplicate checking now that the Earley Parse
algorithm is in use.) Plus<code> mmj.verify.BottomUpParser.java</code>
can be eliminated without loss. <br>
  </li>
  <li>Unification in the mmj2 Proof Assistant depends upon there being
a single, unique syntax tree for each valid expression. Grammatical
productions intended to support things like "x + y + z" in an
unambiguous manner may possibly be defined away using "Syntax Proofs",
but little work has been done in this area beyond dealing with
weq/wceq, etc. in set.mm for the mmj2 Proof Assistant project (see <a
 href="doc/BasicsOfSyntaxAxiomsAndTypes.html">BasicsOfSyntaxAxiomsAndTypes.html</a>).</li>
</ul>
<br>
<big><span style="font-weight: bold;">6.</span></big> <span
 style="font-weight: bold;">Next Steps, Possible Enhancements, and
Experimental Topics:</span><br>
<br>
<ul>
  <li>Enhance the mmj2 Service Feature by adding a Ctrl key on the mmj2
Proof Assistant GUI screen to invoke the current mmj2 Service program
(plug-in) program, passing the proof worksheet as input. Upon return
from the invoked program, the mmj2 Proof Assistant GUI would unify the
(possibly) modified proof worksheet and display the results. The would
be one way to connect mmj2 and a user-written step "prover" (or other
useful proof modifier).</li>
  <li><big style="color: rgb(204, 51, 204);"><big>?</big></big><br>
  </li>
</ul>
<br>
<big><span style="font-weight: bold;">7.</span></big> <span
 style="font-weight: bold;">Acknowledgements:</span><br>
<ul>
  <li>Norman Megill, Legendary Inventor of Metamath&nbsp; [<a
 href="http://www.metamath.org">http://www.metamath.org</a>] <br>
  </li>
  <li>Raph Levien [<a href="http://www.levien.com/">http://www.levien.com/</a>],
Inventor
of






    <code>mmverify.py</code> and Ghilbert&nbsp; [<a
 href="http://ghilbert.org/">http://ghilbert.org/</a>]</li>
  <li>Robert M. Solovay, Author of <code>peano.mm</code> [<a
 href="http://math.berkeley.edu/%7Esolovay/">http://math.berkeley.edu/~solovay/</a>]</li>
  <li>Dick Grune and Ceriel J.H. Jacobs, Authors of "Parsing Techniques
- A Practical Guide" [<a href="http://www.cs.vu.nl/%7Edick/PTAPG.html">http://www.cs.vu.nl/~dick/PTAPG.html</a>]</li>
  <li>Aaron Krowne and Joe Corneli, PlanetMath [<a
 href="http://planetmath.org/">http://planetmath.org/</a>], the
original sponsors of mmj2<br>
  </li>
  <li> Herbert B. Enderton, Author of "A Mathematical Introduction to
Logic" (1972, Academic Press)<br>
  </li>
  <li>&nbsp;[<a href="http://www.math.ucla.edu/%7Ehbe/amil/index.html">http://www.math.ucla.edu/~hbe/amil/index.html</a>]</li>
  <li>Richmond H. Thomason, Author of&nbsp; "Symbolic Logic, An
Introduction" (1970, Macmillan)<br>
  </li>
  <li>Professor Vann McGee, <a
 href="http://ocw.mit.edu/OcwWeb/Linguistics-and-Philosophy/24-241Logic-IFall2002/CourseHome/index.htm">MIT
Open
Courseware,
Logic
I</a></li>
  <li>Michael Beeson, Explainer Extraordinaire of Unification&nbsp; [<a
 href="http://michaelbeeson.com/research/otter-lambda/index.php?include=Unification">http://michaelbeeson.com/research/otter-lambda/index.php?include=Unification</a>]








    <br>
  </li>
  <li>Alin Suciu, Yet Another Efficient Unification Algorithm [<a
 href="http://arxiv.org/pdf/cs/0603080">http://arxiv.org/pdf/cs/0603080</a>]<a
 class="url" href="http://arxiv.org/pdf/cs/0603080"><br>
    </a></li>
  <li>F. Line, Paul Chapman and many others who provided analysis,
feedback, ideas, review and/or testing.<br>
  </li>
  <li>Sci-Fi Inspiration: Greg Egan, "<a
 href="http://gregegan.customer.netspace.net.au/DIASPORA/DIASPORA.html">Diaspora</a>";
Charles
Stross,
"<a
 href="http://www.antipope.org/charlie/blog-static/fiction/accelerando/accelerando-intro.html">Accelerando</a>";
Bruce
Sterling,
"<a
 href="http://www.amazon.com/Distraction-Bruce-Sterling/dp/0553576399">Distraction</a>";
Neal
Stephenson,
"<a
 href="http://www.amazon.com/Snow-Crash-Bantam-Spectra-Book/dp/0553380958">Snow
Crash</a>"; and Robert Heinlein, "<a
 href="http://www.amazon.com/Assignment-Eternity-Robert-Heinlein/dp/0671578650">Gulf</a>".</li>
  <li>Everyone else I forgot to list. Thanks! <br>
  </li>
</ul>
<br>
<br>
<br>
<br>
</body>
</html>
